\begin{tabbing}
w{-}machine{-}constraint($w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:Id.\+
\\[0ex]let ${\it Choose}$,${\it Trans}$,${\it Send}$ = w{-}machine($w$;$i$) in 
\\[0ex]$\forall$$t$:$\mathbb{N}$.
\\[0ex]($\neg$($\uparrow$w{-}isnull($w$; w{-}a($w$; $i$; $t$))))
\\[0ex]$\Rightarrow$ \=(\=($\lambda$$x$.w{-}s($w$; $i$; ($t$+1); $x$))\+\+
\\[0ex]=
\\[0ex]($\lambda$$x$,$q$. \=${\it Trans}$\+
\\[0ex](w{-}kind($w$; w{-}a($w$; $i$; $t$))
\\[0ex],w{-}val($w$; w{-}a($w$; $i$; $t$))
\\[0ex],$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)
\\[0ex],$x$
\\[0ex],$q$ + 1))
\-\\[0ex]$\in$ $x$:Id$\rightarrow\mathbb{Q}\rightarrow$w{-}vartype($w$; $i$; $x$)
\-\\[0ex]\& (\=($\uparrow$islocal(w{-}kind($w$; w{-}a($w$; $i$; $t$))))\+
\\[0ex]$\Rightarrow$ ($\exists$\=$x$:$\mathbb{N}$\+
\\[0ex](($\uparrow$isl(${\it Choose}$(act(w{-}kind($w$; w{-}a($w$; $i$; $t$))),$x$,$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)(0))))
\\[0ex]c$\wedge$ (\=w{-}val($w$; w{-}a($w$; $i$; $t$))\+
\\[0ex]=
\\[0ex]outl(${\it Choose}$(act(w{-}kind($w$; w{-}a($w$; $i$; $t$))),$x$,$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)(0)))
\\[0ex]$\in$ w{-}valtype($w$; $i$; w{-}a($w$; $i$; $t$))))))
\-\-\-\\[0ex]\& \=w{-}m($w$; $i$; $t$)\+
\\[0ex]=
\\[0ex]${\it Send}$(w{-}kind($w$; w{-}a($w$; $i$; $t$)),w{-}val($w$; w{-}a($w$; $i$; $t$)),$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)(0))
\\[0ex]$\in$ (Msg($w$.M) List))
\-\-\-
\end{tabbing}